i:Id, L:(Knd List), x:Id. @i: only members of L read x  Dsys 

latex

Definitions	Id, t  T, Knd, type List, , x:A. B(x), only members of L read x, MsgA, IdDeq, eqof(d), f(a), if b then t else f fi , x.A(x), @i: only members of L read x, Dsys
Lemmas	ifthenelse wf, eqof wf, id-deq wf, msga wf, ma-single-rframe wf, ma-empty wf, Knd wf, Id wf